(set-logic QF_UF)   
(declare-sort a 0)  
(declare-fun b (a a) a) 
(declare-fun c () a) 
(declare-fun d () a) 
(declare-fun l () a) 
(declare-fun e () a) 
(declare-fun f () a) 
(assert (let ( (?g (b e e)) (?h (b e l)) (?i (b l l)) (?j (b l d)) (?k (b d c))) 
(and (and (and (and  (and (and (and (and (or (or (or  (= ?g l))) )
(or (or  (= ?h l)) (= ?h d))   (= ?i d)))(or (or (or  (= ?j e)) (= ?j l)) (= ?j d)) )))
(or (or (or  (= ?k l)) (= ?k d)) (= ?k c)))   
(not (= (b l l) l))   
(and (and (and (and (and (and  (and (= f l)  
(and (and (and (and  (= (b l l) f)) ) ) ) ) ) ) ) ) ) ) ) ))) 
(check-sat)

